A, B:MsgA. (A ||+ B)  (B ||+ A) 

latex

Definitions	t  T, P  Q, x:A. B(x), MsgA, ma-frame-compatible(A;B), M1 || M2, x:AB(x), Prop, P & Q, A ||+ B
Lemmas	ma-compatible wf, ma-frame-compatible wf, msga wf, ma-frame-compatible symmetry, ma-compatible-symmetry